R:es_realizer{i:l}, y,i:Id. (read-restricted(R; i; y))  (R-has-loc(R; i)) 

latex

Definitions	t  T, P  Q, x:A. B(x), prop{i:l}
Lemmas	es realizer wf, Id wf, read-restricted wf, assert wf, read-restricted-R-occurs, R-occurs-has-loc